$\forall$${\it es}$:ES, $i$, $x$:Id, $T$, $A$:Type, $f$:($T$$\rightarrow$$A$).
\\[0ex]vartype($i$;$x$) $\subseteq\rho$ $T$
\\[0ex]$\Rightarrow$ $\forall$$e$@$i$. $f$(($x$ after $e$)) $=$ $f$($x$ when $e$)
\\[0ex]$\Rightarrow$ $\forall$$e$@$i$. $f$($x$ when $e$) $=$ $f$($x$ when es{-}init(${\it es}$;$e$))